feat(Logic): logical operators#607
Conversation
fmontesi
changed the title
| public import Cslib.Foundations.Logic.Operators.Not | ||
| public import Cslib.Foundations.Logic.Operators.Box | ||
| public import Cslib.Foundations.Logic.Operators.Diamond | ||
| public import Cslib.Foundations.Logic.Operators.Iff |
There was a problem hiding this comment.
Would it be better to just have one file for these? If they're just notation typeclasses it seems unlikely to be heavyweight and they're likely to be used together.
There was a problem hiding this comment.
I don't know yet. We will expand these files with extended classes for expected properties about these operators, but you're right that some will require importing more than one.. I think we'll know more once we get there.
There was a problem hiding this comment.
I propose 3 files:
Modalcontaining box and diamond.Tensorby itself.Propositionalfor the reset.
BTW, do we need parameterized box and diamond for HML?
The class was intentionally uninstantiated dead code. Its neg/top rationale (minimal-logic validity) now lives in the module docstring; formula types define neg/top as abbrevs directly. Future generic abstractions should use PR leanprover#607-style HasNeg/HasTop atomic classes. Session: sess_1781312776_63c955
The class was intentionally uninstantiated dead code. Its neg/top rationale (minimal-logic validity) now lives in the module docstring; formula types define neg/top as abbrevs directly. Future generic abstractions should use PR leanprover#607-style HasNeg/HasTop atomic classes. Session: sess_1781312776_63c955
Upstream PR landscape audit for Modal/ logic. No competing signature-change PRs. PR leanprover#607 stalled with CHANGES_REQUESTED. Recommends stacking Modal PR on feat/temporal-formula-propositional. Session: sess_1781531573_4cdbb4
Diplomatic PR description for Modal/ formula primitives refactoring, stacking on PR leanprover#648. Coordinates with PRs leanprover#607, leanprover#528, leanprover#535, leanprover#649. Session: sess_1781535860_c7d8e9
|
Hi @fmontesi — I wanted to flag some overlap with PR #648 so we can coordinate. PR #648 includes The main naming difference is A follow-up to #648 would refactor the Modal constructors from |
There was a problem hiding this comment.
I'd suggest merging all these operators into a single LogicOperators file, since then you can give one docstring that summarizes the conventions of their meanings.
| @[inherit_doc] scoped infix:35 " ∨ " => Proposition.or | ||
| @[inherit_doc] scoped infix:30 " → " => Proposition.impl | ||
| @[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg | ||
| instance : HasAnd (Proposition Atom) := {and := Proposition.and} |
There was a problem hiding this comment.
A little cleaner as
| instance : HasAnd (Proposition Atom) := {and := Proposition.and} | |
| instance : HasAnd (Proposition Atom) where and := .and |
etc
| induction ctx <;> grind [= Context.fill] | ||
|
|
||
| noncomputable instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where | ||
| noncomputable instance : HasLogicalEquivalence (Proposition Atom) (Sequent Atom) where |
There was a problem hiding this comment.
Note that the Has prefix is largely a Lean 3-ism.
There was a problem hiding this comment.
We use HasX for 'canonical' versions of X for a type, whenever X is instead parametrised over the target type, also in other typeclasses.
…#648 refresh Recreates the four tasks lost during the main cleanup, aligned with Thomas Waring's closing recommendation in the CSLib Zulip "Propositional Logic" thread (606970606) and our synthesis decision: - 398 efq_nd_rule_ipl_base_keep_mpl: make IPL the base logic (efq as a primitive ND rule) while PRESERVING all completed MPL metatheory as a retained layer. Depends on 397 (green main). - 399 refresh_pr648_ipl_base_foundation: update PR leanprover#648 to the settled IPL-base foundation (refs + Zulip link), small + upstream-based cherry pick, connectives excluded. Depends on 398. - 400 reconcile_connectives_pr607: unbundle connectives, reconcile with fmontesi PR leanprover#607 (Waring flag a). - 401 polymorphic_evaluator_bool_prop_dpll: AlgEvaluate at Bool/Prop for DPLL (Doty/Waring). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NarRy36MgZCZP7TRsrL5Df
… falso Promote ex falso quodlibet (bottom-elimination) to an ungated primitive constructor of the natural-deduction Derivation, so IPL is the base propositional logic and the primitive bot constructor has an inference rule. IPL becomes the empty base theory; CPL still adds double negation elimination. The minimal-logic (MPL) layer is deferred to a separate PR: this removes MPL, the IsIntuitionistic typeclass, intuitionisticCompletion, and the derived efq rules, keeping the classical layer (byContra/lem/pierce and the IsClassical instances for CPL/LEM/Pierce) intact, re-proved via the efq constructor. Per reviewer feedback (Waring, CSLib Zulip 'Propositional Logic'): - Drop the connective typeclasses (Foundations/Logic/Connectives.lean and its registration instances) -- a separate development handled via PR leanprover#607. - Restore references (Gentzen 1935, Prawitz 1965, Troelstra-van Dalen 1988) and add the CSLib Zulip thread link. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019sHZHp7U5qSiEzioK1nGEH
… falso Promote ex falso quodlibet (bottom-elimination) to an ungated primitive constructor of the natural-deduction Derivation, so IPL is the base propositional logic and the primitive bot constructor has an inference rule. IPL becomes the empty base theory; CPL still adds double negation elimination. The minimal-logic (MPL) layer is deferred to a separate PR: this removes MPL, the IsIntuitionistic typeclass, intuitionisticCompletion, and the derived efq rules, keeping the classical layer (byContra/lem/pierce and the IsClassical instances for CPL/LEM/Pierce) intact, re-proved via the efq constructor. Per reviewer feedback (Waring, CSLib Zulip 'Propositional Logic'): - Drop the connective typeclasses (Foundations/Logic/Connectives.lean and its registration instances) -- a separate development handled via PR leanprover#607. - Restore references (Gentzen 1935, Prawitz 1965, Troelstra-van Dalen 1988) and add the CSLib Zulip thread link. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019sHZHp7U5qSiEzioK1nGEH
… falso Promote ex falso quodlibet (bottom-elimination) to an ungated primitive constructor of the natural-deduction Derivation, so IPL is the base propositional logic and the primitive bot constructor has an inference rule. IPL becomes the empty base theory; CPL still adds double negation elimination. The minimal-logic (MPL) layer is deferred to a separate PR: this removes MPL, the IsIntuitionistic typeclass, intuitionisticCompletion, and the derived efq rules, keeping the classical layer (byContra/lem/pierce and the IsClassical instances for CPL/LEM/Pierce) intact, re-proved via the efq constructor. Per reviewer feedback (Waring, CSLib Zulip 'Propositional Logic'): - Drop the connective typeclasses (Foundations/Logic/Connectives.lean and its registration instances) -- a separate development handled via PR leanprover#607. - Restore references (Gentzen 1935, Prawitz 1965, Troelstra-van Dalen 1988) and add the CSLib Zulip thread link. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019sHZHp7U5qSiEzioK1nGEH
|
Following up on my comment above: the overlap I flagged is now resolved on #648's side — I've removed the connective typeclasses from #648, so it no longer duplicates the classes in this PR. #648 now contributes the five-primitive That leaves one spot where the two PRs still meet: your head has since its own I'd favor the primitive Two smaller notes: I'd keep the |
… falso Promote ex falso quodlibet (bottom-elimination) to an ungated primitive constructor of the natural-deduction Derivation, so IPL is the base propositional logic and the primitive bot constructor has an inference rule. IPL becomes the empty base theory; CPL still adds double negation elimination. The minimal-logic (MPL) layer is deferred to a separate PR: this removes MPL, the IsIntuitionistic typeclass, intuitionisticCompletion, and the derived efq rules, keeping the classical layer (byContra/lem/pierce and the IsClassical instances for CPL/LEM/Pierce) intact, re-proved via the efq constructor. Per reviewer feedback (Waring, CSLib Zulip 'Propositional Logic'): - Drop the connective typeclasses (Foundations/Logic/Connectives.lean and its registration instances) -- a separate development handled via PR leanprover#607. - Restore references (Gentzen 1935, Prawitz 1965, Troelstra-van Dalen 1988) and add the CSLib Zulip thread link. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019sHZHp7U5qSiEzioK1nGEH
…-neg point) Add engagement report + concrete review points for fmontesi PR leanprover#607: the primary HasBot-vs-primitive-HasNot design issue for IPL/MPL, plus naming, notation-precedence, and bundling deltas. Note prereq done -- Connectives.lean removed from leanprover#648 (commit 85db79a6). Status -> researched. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019sHZHp7U5qSiEzioK1nGEH
Rewrite pr-description.md and zulip-response.md to match the shipped design: ungated primitive efq (IPL is the base), minimal/MPL deferred (not 'retained as fragment'), Theory.lean kept (not deleted), connectives removed (PR leanprover#607), 4 references added, fast-forward update (no force-push). Human-author banners preserved per Zulip AI policy. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019sHZHp7U5qSiEzioK1nGEH
Re-research pass grounded in live PR leanprover#607 diff + review thread. Recommends incremental engagement (not a competing architecture): reuse Mathlib Bot/Top, derived-negation bridge, human-authorable review skeleton. Session: sess_1782754611_b50d40
Human-authorable drafts (Zulip AI policy) for engaging PR leanprover#607: incremental strategy — reuse Mathlib Bot/Top + derived-neg bridge, naming/_def/precedence points, bundles as follow-up. Session: sess_1782754611_b50d40
…description Replace "a HasBot class is needed" with the corrected position (reuse Mathlib Bot/Top + derived HasNot + (φ → ⊥)=¬φ grind bridge, no HasBot). Aligns the leanprover#648 body with task 400's report 02 / pr-response / zulip-response. Also pushed to the live PR leanprover#648 body. Session: sess_1782754611_b50d40
…m self-correction Lead with leanprover#648 status (efq/IPL-base, deferrals, connectives out), self-correct the falsum framing (reuse Mathlib Bot/Top, no HasBot) to match leanprover#607 review, and note imp/impI/impE is settled in leanprover#648. Session: sess_1782754611_b50d40
Drop the detailed leanprover#607 falsum/naming/precedence discussion; keep only the brief "will review leanprover#607 to help it land" line. Detailed leanprover#607 engagement moves to a later follow-up comment. Session: sess_1782754611_b50d40
Address Waring's four points: accept the efq-primitive/IPL-base compromise (done in leanprover#648), agree fragment design is deferred (manipulations carry over by spec), connectives out -> brief leanprover#607 mention, and confirm references + Zulip link now in the PR (his missing-refs flag). Session: sess_1782754611_b50d40
…r#607 Phase 1: comparison tables (HasX classes, notation divergences, naming options, precedence ladder, file-org options, prior-comment anchor). Phase 2: falsum bridge sketch with verified Lean (HasNot + Bot/Top reuse; (A → ⊥) = HasNot.not A is rfl; explicit retraction of HasBot proposal). Phase 3: empirical grind-through-notation finding: - POSITIVE: grind alone closes Satisfies.and_iff and Satisfies.dual for the fork's Modal.Proposition (abbrev-based derived connectives). - NEGATIVE: simp/grind fail for upstream-like primitive-constructor+ typeclass-wrapper architecture without explicit instance bridge. - Diagnosis: chenson's orientation (constructor→notation) worsens grind for the upstream case; notation→constructor helps. Phase 4: consolidated 04_review-packet.md ordered by report-02 §6 priority, anchored on prior comment, all verified exhibits embedded. No production Lean modified; scratch files created and deleted after verification. Phases 5-8 remain as-is (human/external/conditional gates). Session: sess_1782759395_5a8840
…eanprover#607 review Session: sess_1782759395_5a8840
6 participants
This PR introduces typeclasses for logical operators (connectives and modalities) and refactors modal and propositional logics with appropriate instances to these.